COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	declare INDCONST RW ε WORLD
C00007 ENDMK
C⊗;
declare INDCONST RW ε WORLD;
declare INDVAR w w1 w2 w3 w4 w5 ε WORLD;
declare INDVAR m n m1 m2 m3 n1 n2 n3 ε NATNUM;

declare INDCONST W1 W2 W3 W123 ε PERSON;
declare INDVAR p p0 p1 p2 ε PERSON;

declare PREDCONST A(WORLD,WORLD,PERSON,NATNUM);

declare INDVAR c c1 c2 c3 c4 ε COLORS;
declare INDCONST W B ε COLORS;

declare OPCONST color(PERSON,WORLD) = COLORS;

axiom reflex:	∀w p m.A(w,w,p,m);;

axiom transitive:	∀w1 w2 w3 p m.(A(w1,w2,p,m) ∧ A(w2,w3,p,m) ⊃ A(w1,w3,p,m));;

axiom who:	∀p.(p=W1 ∨ p=W2 ∨ p=W3 ∨ p=W123);;

axiom w123:	∀w1 w2 m.(A(w1,w2,W1,m) ∨ A(w1,w2,W2,m) ∨ A(w1,w2,W3,m)
			⊃ A(w1,w2,W123,m))
;;

axiom foolscap:	∀w.(color(W123,w)=W);;

axiom color:	¬(W=B)
		∀c.(c=W ∨ c=B)
;;

axiom rw:	color(W1,RW) = W ∧ color(W2,RW) = W ∧ color(W3,RW) = W;;

axiom initial:	∀c w.(A(RW,w,W123,0) ⊃
	(c=W ∨ color(W2,w)=W ∨ color(W3,w)=W
		⊃ ∃w1.(A(w,w1,W1,0) ∧ color(W1,w1) = c)) ∧
	(c=W ∨ color(W1,w)=W ∨ color(W3,w)=W
		⊃ ∃w1.(A(w,w1,W2,0) ∧ color(W2,w1) = c)) ∧
	(c=W ∨ color(W1,w)=W ∨ color(W2,w)=W
		⊃ ∃w1.(A(w,w1,W3,0) ∧ color(W3,w1) = c)))

	∀w w1.(A(RW,w,W123,0) ∧ A(w,w1,W1,0)
		⊃ color(W2,w1) = color(W2,w) ∧ color(W3,w1) = color(W3,w))

	∀w w1.(A(RW,w,W123,0) ∧ A(w,w1,W2,0)
		⊃ color(W1,w1) = color(W1,w) ∧ color(W3,w1) = color(W3,w))

	∀w w1.(A(RW,w,W123,0) ∧ A(w,w1,W3,0)
		⊃ color(W1,w1) = color(W1,w) ∧ color(W2,w1) = color(W2,w))
;;

comment :  initial establishes the existence of enough possible worlds. :

axiom king:	∀w.(A(RW,w,W123,0) ⊃ color(W1,w)=W ∨ color(W2,w)=W
			∨ color(W3,w)=W);;

axiom elwek1:	∀w.(A(RW,w,W123,1) ≡ A(RW,w,W123,0) ∧
	∀p.(∀w1.(A(w,w1,p,0) ⊃ color(p,w1)=color(p,w)) ≡ ∀w1.(A(RW,w1,p,0)
⊃ color(p,w1)=color(p,RW))))

	∀w1 w2.(A(w1,w2,W1,1) ≡ A(w1,w2,W1,0) ∧ A(w1,w2,W123,1))
	∀w1 w2.(A(w1,w2,W2,1) ≡ A(w1,w2,W2,0) ∧ A(w1,w2,W123,1))
	∀w1 w2.(A(w1,w2,W3,1) ≡ A(w1,w2,W3,0) ∧ A(w1,w2,W123,1))
;;

axiom elwek2:	∀w.(A(RW,w,W123,2) ≡ A(RW,w,W123,1) ∧
	∀p.(∀w1.(A(w,w1,p,1) ⊃ color(p,w1)=color(p,w)) ≡ ∀w1.(A(RW,w1,p,1)
⊃ color(p,w1)=color(p,RW))))

	∀w1 w2.(A(w1,w2,W1,2) ≡ A(w1,w2,W1,1) ∧ A(w1,w2,W123,1))
	∀w1 w2.(A(w1,w2,W2,2) ≡ A(w1,w2,W2,1) ∧ A(w1,w2,W123,1))
	∀w1 w2.(A(w1,w2,W3,2) ≡ A(w1,w2,W3,1) ∧ A(w1,w2,W123,1))
;;
COMMENT : elwek1 and elwek 2 thell what happens when everyone learns
whether everyone else knows the color of his spot.  The sentence starting ∀p.
says that p knows the color of his spot in w iff he knows it in RW. :